『Introduction to Homotopy Type Theory』

#2022年

E. Rijke, “Introduction to Homotopy Type Theory”. Dec. 21, 2022, arXiv: arXiv:2212.11082. doi: 10.48550/arXiv.2212.11082.

【2212.11082】 Introduction to Homotopy Type Theory. 2022.

著者：Rijke Egbert

タイトル: Introduction to Homotopy Type Theory

identity type(同一視型)はMartin-Löf型理論の最も特徴的な型

依存型理論の4つの推論規則、形成規則(formation rule)、導入規則(introduction rule)、除去規則(elimination rule)、計算規則(computation rule)のほかに、判断としての等しさ(judgmental equality)を保証するための合同ルール(congruence rule)というものがある

∞-トポス

Kan simplicial set(カン単体的集合？)

単体的集合

『The simplicial model of univalent foundations (after Voevodsky)』(arXiv)

Krzysztof Kapulkin and Peter LeFanu Lumsdaine. “The simplicial model of univalent foundations (after Voevodsky)”. In: J. Eur. Math. Soc. (JEMS) 23.6 (2021), pp. 2071–2126. issn: 1435-9855. doi: 10.4171/JEMS/ 1050. url: https://doi.org/10.4171/JEMS/1050.

『SymmetryBook』

Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson. Symmetry. . 2022.

(higher) group theory

$ \frac{\mathcal{H}_1 \quad \mathcal{H}_2 \quad ... \quad \mathcal{H}_n}{ \mathcal{C}}

$ \mathcal{H}_1 \quad \mathcal{H}_2 \quad ... \quad \mathcal{H}_n : 前提(premises)

$ \mathcal{C} : 結論(conclusion)

============================

Martin-Löf依存型理論の4種類の判断(judgments)がある

(1) $ \Gamma \vdash A \ type

Aは文脈$ \Gamma 中の(well-formedな)型(type)

(2) $ \Gamma \vdash A \ \dot{=} \ B \ type

AとBは文脈$ \Gamma 中のjudgmentally equal型

(3) $ \Gamma \vdash a : A

aは文脈$ \Gamma 中の要素(element)

(4) $ \Gamma \vdash a \ \dot{=} \ b \ type

aとbは文脈$ \Gamma 中のjudgmentally equal要素

judgmentally equalなものはドット付きのものでわかるようにしてるっぽい

$ \Gamma \vdash A \ \dot{=} \ B \ type

以下のようなものは判断の例

$ \Gamma \vdash a : A

$ \Gamma \vdash f : A \to B

$ \Gamma \vdash f(a) : B

============================

型の推移律と、要素の推移律がある

$ \frac{\Gamma \vdash A\ \dot{=}\ B\ \text{type}\quad \Gamma \vdash B\ \dot{=}\ C\ \text{type}}{\Gamma \vdash A\ \dot{=}\ C \ \text{type}}

$ \frac{\Gamma \vdash a\ \dot{=}\ b: A\quad \Gamma \vdash b\ \dot{=}\ c: A}{\Gamma \vdash a\ \dot{=}\ c: A}

次の読むべき論文？

『All (∞, 1)-toposes have strict univalent universes』

『Homotopy theoretic models of identity types』

arXiv: https://arxiv.org/abs/0709.0248

#依存型理論

#Homotopy_Type_Theoryの参考文献

#文献